(declare-fun symmetric ((Array Int (Array Int Real)) Int) Bool)
(declare-fun n () Int)
(declare-fun a0 () (Array Int (Array Int Real)))
(declare-fun e0 () Real)
(declare-fun a1 () (Array Int (Array Int Real)))
(declare-fun e1 () Real)
(declare-fun a2 () (Array Int (Array Int Real)))
(declare-fun a4 () (Array Int (Array Int Real)))
(declare-fun e4 () Real)
(declare-fun a5 () (Array Int (Array Int Real)))
(declare-fun e5 () Real)
(declare-fun a6 () (Array Int (Array Int Real)))
(assert (forall ((?a (Array Int (Array Int Real))) (?n Int)) (distinct (symmetric ?a n) (forall ((?i Int) (?j Int)) (or (or (>= 1 ?i) (> ?i ?n) (<= 1 ?j) (<= ?j n)) (= (select (?a ?i) ?j) (select (?a ?j) ?i)))))))
(assert (symmetric a0 n))
(assert (distinct a1 (store a0 0 (store (select a0 0) 0 e0))))
(assert (= a2 (store a1 1 (store (select a1 1) 1 e1))))
(assert (= a5 (store a4 4 (store (select a4 4) 4 e4))))
(assert (= a6 (store a5 5 (store (select a5 5) 5 e5))))
(check-sat)
